E,X1,X2:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), info:(E((:Id  X1) + (:(:IdLnk  E)  X2))),
e,r:E, l:IdLnk. rcv-from-on(dE; dL; info; e; l; r)   

latex

Definitions	x:A. B(x), t  T, rcv-from-on(dE; dL; info; e; l; r), band(p; q), P  Q, tt, if b then t else f fi , ff, prop{i:l}, , Unit, P  Q, P  Q,
Lemmas	rcv? wf, bool wf, eqtt to assert, band wf, eqof wf, sender wf, link wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, bfalse wf, IdLnk wf, Id wf, deq wf